$\forall$$A$:Realizer. Rplus?($A$) $\Rightarrow$ ($A$ $\sim$ (Rplus{-}left($A$) $\oplus$ Rplus{-}right($A$)))